$\forall$${\it es}$:ES, $e$, ${\it e'}$:E, $l$:IdLnk.
\\[0ex](${\it e'}$ $\in$ es{-}receives(${\it es}$;$e$;$l$)) $\Leftrightarrow$ isrcv(${\it e'}$) \& sender(${\it e'}$) $=$ $e$ \& lnk(${\it e'}$) $=$ $l$